#include <boost/config/warning_disable.hpp>

#include <boost/spirit/include/qi.hpp>
#include <boost/spirit/include/phoenix_operator.hpp>
#include <boost/bind.hpp>

#include <boost/graph/adjacency_list.hpp>
#include <boost/graph/directed_graph.hpp>
#include <boost/graph/tiernan_all_cycles.hpp>
#include <boost/graph/graphviz.hpp>
#include "../include/helper.hpp"
#include <boost/program_options.hpp>

#include <iostream>
#include <string>
#include <algorithm>
#include <vector>

namespace machine{

	struct property_t {
  		typedef boost::vertex_property_tag kind;
	};

	struct name_t { 
  		typedef boost::vertex_property_tag kind;
	};

	struct marks_t { 
  		typedef boost::vertex_property_tag kind;
	};

	typedef boost::property<property_t, std::string> Prop;
	typedef boost::property<marks_t, std::vector<int>, Prop> Prop2;
  	typedef boost::property<name_t, std::string, Prop2> VertexProperty;	
	typedef boost::directed_graph<VertexProperty> Graph;
	typedef boost::graph_traits<Graph>::vertex_iterator vertex_iter;
	typedef typename boost::graph_traits<Graph>::adjacency_iterator adjacency_iterator;	
	
	class MachineCTL{
	public:

		MachineCTL(std::string fileDot){
		
			Graph g;
	
			boost::dynamic_properties dp;
			boost::property_map<Graph, name_t>::type name = 
				boost::get(name_t(), g);
			boost::property_map<Graph, property_t>::type label = 
				boost::get(property_t(), g);
  	
			dp.property("node_id",name);
  			dp.property("comment",label);

			std::string filename = fileDot;
 			std::ifstream fin(filename.c_str());
	
			boost::read_graphviz(fin,g,dp,"node_id");

			std::cout << "Properties of states: "<< std::endl;
    		std::pair<vertex_iter, vertex_iter> vp;
    		for (vp = vertices(g); vp.first != vp.second; ++vp.first){
					std::cout << get(name_t(),g,*vp.first)<< ": " << get(property_t(),g,*vp.first) <<  std::endl;
					std::string properties = boost::get(property_t(),g,*vp.first);
					properties += ",T";
					boost::put(property_t(),g,*vp.first,properties);
			}

			this->g = g;
		}

		int getNumVertices(){
			return num_vertices(g);
		}
		
		void getAllMarksByState(){
	
    		std::pair<vertex_iter, vertex_iter> vp;
			std::vector<int> marks;
			
        	std::cout << "----------------------------------------------------------\n";
			std::cout << "Marks by State: " << std::endl;
			
			for (vp = vertices(g); vp.first != vp.second; ++vp.first){

					marks = boost::get(marks_t(),g,*vp.first);
					std::cout <<  get(name_t(),g,*vp.first) << ": ";
				    
					std::vector<int>::iterator it;
					std::vector<int>  array;
					for(it = marks.begin(); it != marks.end(); it++){
							if(!hasElement(array,*it) || array.size() == 0 ){
								array.push_back(*it);	
							} 
					}
					
					for(it = array.begin(); it != array.end(); it++){
						std::cout << *it << " ";	
					}

					std::cout << std::endl;
			}
		
		}

		void property(std::string const& prop,int const mark){

    		std::pair<vertex_iter, vertex_iter> vp;
    		std::string properties;
			std::vector<int> marks;
			for (vp = vertices(g); vp.first != vp.second; ++vp.first){
					properties = boost::get(property_t(),g,*vp.first);
					if( properties.find(prop) != std::string::npos ){
							marks = boost::get(marks_t(),g,*vp.first);
							marks.push_back(mark);
							boost::put(marks_t(),g,*vp.first,marks);
					} 	
			}
		/*	
			for (vp = vertices(g); vp.first != vp.second; ++vp.first){
					marks = boost::get(marks_t(),g,*vp.first);
					std::vector<int>::iterator it;
					std::cout <<  get(name_t(),g,*vp.first) << " ";
					for(it = marks.begin(); it != marks.end(); it++){
						std::cout << *it << " ";  
					}
					std::cout << std::endl;
			}
		*/
		}

		void af(int const mark, int const markAF){
			
			std::pair<vertex_iter, vertex_iter> vp;
			adjacency_iterator begin, end;
			std::vector<int> marks;

			for (vp = vertices(g); vp.first != vp.second; ++vp.first){

				marks = boost::get(marks_t(),g,*vp.first);
				boost::tie(begin, end )= boost::adjacent_vertices(*vp.first, g);
	
				if( hasElement(marks,mark) ||  hasAf( begin, end, markAF) ){
					marks.push_back(markAF);
					boost::put(marks_t(),g,*vp.first,marks);
				}
			
			}
		}
		
		void ex(int const mark,int const markEx){

			std::pair<vertex_iter, vertex_iter> vp;
			adjacency_iterator begin, end;
			std::vector<int> marks;

			for (vp = vertices(g); vp.first != vp.second; ++vp.first){

				marks = boost::get(marks_t(),g,*vp.first);
				boost::tie(begin, end )= boost::adjacent_vertices(*vp.first, g);
	
				if( hasEx( begin, end, mark) ){
					marks.push_back(markEx);
					boost::put(marks_t(),g,*vp.first,marks);
				}
			
			}
		}

		void eu(int const mark1, int const mark2, int const markEu){
			
			std::pair<vertex_iter, vertex_iter> vp;
			adjacency_iterator begin, end;
			std::vector<int> marks;

			for (vp = vertices(g); vp.first != vp.second; ++vp.first){

				marks = boost::get(marks_t(),g,*vp.first);
				boost::tie(begin, end )= boost::adjacent_vertices(*vp.first, g);
	
				if( hasElement(marks,mark2) || ( hasElement(marks,mark1)  && hasEu( begin, end, markEu) )){
					marks.push_back(markEu);
					boost::put(marks_t(),g,*vp.first,marks);
				}
			}
		}
		
		void andExp(int const mark1, int const mark2, int const markAnd){
    		
			std::pair<vertex_iter, vertex_iter> vp;
			std::vector<int> marks;
			for (vp = vertices(g); vp.first != vp.second; ++vp.first){
				marks = boost::get(marks_t(),g,*vp.first);
				if( hasElement(marks,mark1) && hasElement(marks,mark2)){
					marks.push_back(markAnd);
					boost::put(marks_t(),g,*vp.first,marks);
				}
			}
		}		
		
		void notExp(int const mark, int const markNot){
    		std::pair<vertex_iter, vertex_iter> vp;
			std::vector<int> marks;
			for (vp = vertices(g); vp.first != vp.second; ++vp.first){
				marks = boost::get(marks_t(),g,*vp.first);
				if( !hasElement(marks,mark) ){
					marks.push_back(markNot);
					boost::put(marks_t(),g,*vp.first,marks);
				}
			}
		}

		void printStateWithProperty(int mark, std::string ctl){
			
			std::pair<vertex_iter, vertex_iter> vp;
			std::vector<int> marks;
			std::vector<std::string> states;
			for (vp = vertices(g); vp.first != vp.second; ++vp.first){
				marks = boost::get(marks_t(),g,*vp.first);
				if( hasElement(marks,mark) ){
					states.push_back(get(name_t(),g,*vp.first));	
				}
			}

        	std::cout << "----------------------------------------------------------\n";
			if( states.size() > 0 ){
				std::cout << "States where the " + ctl +" expression is valid: " << std::endl;
				std::vector<std::string>::iterator it;
				for(it = states.begin(); it != states.end(); ++it )
					std::cout << *it << " ";
				std::cout << std::endl;
			}else{
				std::cout << "The property " + ctl + " isn't valid to given machine" << std::endl; 
				std::cout << " " << std::endl;
			}


		}

	private:

		bool hasEx(adjacency_iterator begin, adjacency_iterator end, int const mark){
			std::vector<int> marks;
			for (  ; begin != end; ++begin){
				marks = boost::get(marks_t(),g,*begin);
				if( hasElement(marks,mark)){
					return true;
				}
			}
			
			return false;
		}

		bool hasEu(adjacency_iterator begin, adjacency_iterator end, int const mark){
			
			std::vector<int> marks;
			for (  ; begin != end; ++begin ){
				marks = boost::get(marks_t(),g,*begin);
				if( hasElement(marks,mark) ){
					return true;
				}
			}

			return false;
		}

		bool hasAf(adjacency_iterator begin, adjacency_iterator end, int const mark){
			
			std::vector<int> marks;
			int has = 0;
			int numAdjacent = 0;

			for (  ; begin != end; ++begin, ++numAdjacent){
				marks = boost::get(marks_t(),g,*begin);
				if( hasElement(marks,mark) ){
					has++;
				}
			}

			return (has == numAdjacent);
		}

		bool hasElement(std::vector<int> array,int mark) {
			if(std::find(array.begin(),array.end(),mark) != array.end() )
				return true;
			else
				return false;
		}

		Graph g;
	};
}

namespace ctlAnalyser {

	namespace qi = boost::spirit::qi;
	namespace ascii = boost::spirit::ascii;

	struct SemanticActionExpression {
	public:

		SemanticActionExpression(){
			mark_number = 1;
		}

		void getAllMarksByState(){
			mCTL->getAllMarksByState();
		}

		void getResult(std::string ctlExp){
				int markFinal = mark_number - 1;
				mCTL->printStateWithProperty(markFinal,ctlExp);
		}

		void viewAllMarks(){
			std::map<std::string,int>::iterator it = marks.begin();
			std::pair < int, std::string > pair;
			std::map<int, std::string> tmpMap;

			for(; it != marks.end(); ++it){
					pair.first = it->second;
					pair.second = it->first;
					tmpMap.insert(pair);
			}

        	std::cout << "----------------------------------------------------------\n";
			std::cout << "Marks: "<< std::endl;
			std::map<int, std::string>::iterator itTmp;
			for(itTmp = tmpMap.begin() ; itTmp != tmpMap.end(); ++itTmp){
				std::cout << itTmp->first << ", " << itTmp->second << std::endl;
			}
			
		}


		void setMachineCTL(machine::MachineCTL *mCTL ){
				this->mCTL = mCTL;
		}

		void prop(std::string const& elem){
			//	std::cout << "PROP" << std::endl;
				addElemToMap(elem);

				int markExp = marks.find(elem)->second;
				mCTL->property(elem,markExp);

		}

		void notExp(std::string const& elem){
			//	std::cout << "NOT" << std::endl;
				
				std::string exp = expression.back();
				expression.pop_back();	
			
				std::string result;
				if ( exp.size() > 1)
					result = "¬(" + exp + ")";
				else
					result = "¬" + exp;
	
				addElemToMap(result);
				int markExp = marks.find(result)->second;
				int mark = marks.find(exp)->second;

				mCTL->notExp(mark,markExp);
				
		}

		void andExp(std::string const& elem, bool computerAnd){
				if( computerAnd ){
					
			//		std::cout << "AND" << std::endl;

					std::string r;
					if (expression.size() > 1 ){
						r = expression.back();
						expression.pop_back();
					}
					
					std::string l = expression.back();
					expression.pop_back();
				
					std::string exp;
					if( l.size() > 1 ){
						exp = "(" + l + ")";
					}
					else{
						exp = l;
					}	
					
					if ( r != "" ){
						if( r.size() > 1 )
							exp += "^(" + r + ")";
						else
							exp += "^"+ r;
					}
					
					addElemToMap(exp);

					int markLeft  = marks.find(l)->second;
					int markRight = marks.find(r)->second;
					int markExp   = marks.find(exp)->second;
				
					mCTL->andExp(markLeft, markRight, markExp);
				//	std::cout << exp << ", " <<  markExp << std::endl;
				}
		}

		void epUq(std::string const& l, std::string const& r) {
				if( l == "" && r == "" ){
					
			//		std::cout << "E[pUq]" << std::endl;

					std::string r;
					if (expression.size() > 1 ){
						r = expression.back();
						expression.pop_back();
					}
					
					std::string l = expression.back();
					expression.pop_back();
				
					std::string exp = "E[";
					if( l.size() > 1 ){
						exp += "("+ l + ")";
					}
					else{
						exp += l;
					}	
					
					if ( r != "" ){
						if( r.size() > 1 )
							exp += "U(" + r + ")]";
						else
							exp += "U"+r + "]" ;
					}
					addElemToMap(exp);

					int markLeft  = marks.find(l)->second;
					int markRight = marks.find(r)->second;
					int markExp   = marks.find(exp)->second;
			
					int numVertices = mCTL->getNumVertices();
					for(int i =0; i < numVertices; i++)	
						mCTL->eu(markLeft, markRight, markExp);
				//	std::cout << exp << ", " <<  markExp << std::endl;
				}
		}	
	
		void af(std::string const& elem){
				if( elem == ""){
			//		std::cout << "AF" << std::endl;

					std::string exp = expression.back();
					expression.pop_back();
					
					std::string result;
					if( exp.size() > 1 ){
						result = "AF(" + exp + ")";	
					}
					else{
						result = "AF" + exp;
					}

					addElemToMap(result);
					int mark = marks.find(exp)->second;
					int markAf   = marks.find(result)->second;

					//std::cout << "mark " << mark <<" markAF " << markAf << std::endl;
					int numVertices = mCTL->getNumVertices();
					for(int i =0; i < numVertices; i++)	
						mCTL->af(mark, markAf);

				}
		}

		void ex(std::string const& elem){
				if( elem == ""){
			//		std::cout << "EF" << std::endl;

					std::string exp = expression.back();
					expression.pop_back();
					
					std::string result;
					if( exp.size() > 1 ){
						result = "EX(" + exp + ")";	
					}
					else{
						result = "EX" + exp;
					}
					
					addElemToMap(result);
					int mark = marks.find(exp)->second;
					int markEx   = marks.find(result)->second;

					mCTL->ex(mark, markEx);
				}
		}
	
	private:

		void addElemToMap(std::string const& elem){
			keyElem.first = elem;
				keyElem.second = mark_number;

			verif = marks.insert ( keyElem );
			if( verif.second ){
				mark_number++;
			}
			
			expression.push_back(elem);
		}


		machine::MachineCTL *mCTL;
		std::vector < std::string > expression;
		std::map  < std::string, int > marks;
		std::pair < std::string, int > keyElem;
		std::pair<std::map<std::string,int>::iterator,bool> verif;
		int mark_number;
	};

	template <typename Iterator>
	struct analyser : qi::grammar<Iterator, std::string()> {
			
		void getAllMarks(){
			sAction.viewAllMarks();
		}

		void getAllMarksByState(){
			sAction.getAllMarksByState();
		}

		void getResult(std::string ctlExp){
			sAction.getResult(ctlExp);
		}

		analyser(std::string fileDot) : analyser::base_type(expression) {
		
			machine::MachineCTL *mCTL = new machine::MachineCTL(fileDot);
			sAction.setMachineCTL(mCTL);
	
			using qi::int_;
			using qi::_val;
			using qi::lit;
        	using qi::double_;
        	using qi::lexeme;
			using qi::eps;
			using qi::ascii::char_;
			using qi::ascii::string;

			property = 
				char_("a-ux-zB-DH-Z"); 

			term =
				eps >>
				( 
					( 
						lit("¬") 
						>> 
						term [boost::bind(&SemanticActionExpression::notExp,&sAction,_1)] 
					)
					|
					factor
				)
				;

			factor =
				eps >>
				(
					property [boost::bind(&SemanticActionExpression::prop,&sAction,_1)] 
					|
                	function
					|
					lit('(') >> expression >> lit(')')
				)
				;
			
			af =
				( string("AF") >> term [boost::bind(&SemanticActionExpression::af,&sAction,_1)] );
		
			ex =
				( string("EX") >> term [boost::bind(&SemanticActionExpression::ex,&sAction,_1)] );				
			
			epuq = 
				( string("E[") 
							>> term 
							>> char_('U') >> term 
							>> char_(']') ) 
						[ 	
							boost::phoenix::ref(l)=qi::_3,
						  	boost::phoenix::ref(r)=qi::_5,
						  	boost::bind(&SemanticActionExpression::epUq,&sAction,l,r)
						];
			
			function = 
				ex  
				|
				af
				|  
				epuq
     			;		
			
			andExp = 
				term [boost::bind(&SemanticActionExpression::andExp,&sAction,_1,false)]  
					>> *( char_('^') 
					>> term [boost::bind(&SemanticActionExpression::andExp,&sAction,_1,true)] );
            
			expression =
				andExp;
				
		}

		qi::rule<Iterator, std::string() > expression, factor, term, property;
		qi::rule<Iterator, std::string() > andExp;
		qi::rule<Iterator, std::string() > function, epuq;
		qi::rule<Iterator, std::string() > ex, af;
		
		SemanticActionExpression sAction;
		
		std::string l, r;
	};
}

namespace ctlReplacer {

	namespace qi = boost::spirit::qi;
	namespace ascii = boost::spirit::ascii;

	struct SemanticActionExpressionSubstitution {
	public:
		
		std::string getExpression(){
			
			std::string exp = expressions.back();
			expressions.pop_back();
			
			return exp;
		}

		void prop(std::string const& elem){
				expressions.push_back(elem);
		}

		void notExp(std::string const& elem){
				std::string exp = expressions.back();
				expressions.pop_back();	
			
				std::string result;
				if ( exp.size() > 1)
					result = "¬(" + exp + ")";
				else
					result = "¬" + exp;

				expressions.push_back(result);
		}

		void impliesExp(std::string const& elem, bool computerImplies){
			creatingimpliesOperator(elem,computerImplies);	
		}

		void andExp(std::string const& elem, bool computerAnd){
			creatingLogicExpressions(elem,"^",computerAnd);
		}
		
		void orExp(std::string const& elem, bool computerOr){
			creatingLogicExpressions(elem,"v",computerOr);
		}
	
		void apUq(std::string const& l, std::string const& r) {
			creatingExpressions(l, r, false);
		}		

		void epUq(std::string const& l, std::string const& r) {
			creatingExpressions(l, r, true);
		}	

		void af(std::string const& elem){
			creatingOperators(elem,"AF");
		}

		void ex(std::string const& elem){
			creatingOperators(elem,"EX");
		}

		void ag(std::string const& elem){
			creatingOperators( elem,"¬E[TU",true,true);
		}
	
		void ax(std::string const& elem){
			creatingOperators(elem,"¬EX¬");
		}

		void ef(std::string const& elem){
			creatingOperators(elem,"E[TU",true);
		}

		void eg(std::string const& elem){
			creatingOperators(elem,"¬AF¬");
		}
/*	
		void left(std::string const& l){
			analysisElement(l,leftElements);	
		}	
		
		void right(std::string const& r){
			analysisElement(r,rightElements);	
		}
*/	
		std::vector<std::string> leftElements, rightElements, expressions;
	
	private:
			void creatingExpressions(std::string const& l, std::string const& r,
										bool isE = false) {
				if( l == "" && r == ""){
					std::string exp = createUntilExpression(isE);
					expressions.push_back(exp);	
				}
				/*
				else {

					if( l == "" || r == "" ){
						if(l == ""){
							right(r);
							std::string exp = createUntilExpression(isE);
						}else if( r == ""){
							left(l);
							std::string exp = createUntilExpression(isE);
						}	
					}
					else{
						left(l);
						right(r);
						std::string exp = createUntilExpression(isE);
					}
				}
				*/
			}
			
			void creatingOperators(std::string const& elem, std::string const& fmt,
										bool hasEnd = false,bool hasNot = false){
				std::string exp = fmt;
				if( elem != ""){
					exp +=  (hasNot?"¬":"") + elem + (hasEnd? "]":"");
					expressions.push_back(exp);
				} 
				else{
					std::string lastExp = expressions.back();
					expressions.pop_back();
					if( lastExp.size() > 1 ){
						exp += (hasNot?"¬(":"(")  + lastExp + ")" + (hasEnd? "]":"");
					}
					else{
						exp += (hasNot?"¬":"") + lastExp + (hasEnd? "]":"");
					}
			
					expressions.push_back(exp);
				}
			}
		
			void creatingLogicExpressions(std::string const& elem, 
							std::string const& op,bool isFinal){
				
				if(!isFinal){
					if( elem != ""){
						std::string exp = elem ;
						expressions.push_back(exp);
					}
				}
				else {
					std::string r, l;
					if(elem != ""){
						r  = elem;
					}
					else{
						std::string opr = expressions.back();
						if ( opr.size() > 1 )	
							r = "(" + opr + ")" ;
						else
							r = opr;
	
						expressions.pop_back();	
					}

					std::string opl = expressions.back();
					if ( opl.size() > 1 )	
						l = "(" + opl + ")" ;
					else
						l = opl;	
						
					expressions.pop_back();	
					
					std::string exp; 
					if( op == "v" ){
						exp += "¬" +l +"^¬" + r +"";
					}
					else{
						exp += l + op + r;
					}
						
					expressions.push_back(exp);
				}
			}	

			void creatingimpliesOperator(std::string const& elem, bool computerImplies){
				if(!computerImplies	){
					if( elem != ""){
						std::string exp = elem ;
						expressions.push_back(exp);
					}
				}
				else{
	
					 std::string r;
				
					if (expressions.size() > 1 ){
						r = expressions.back();
						expressions.pop_back();
					}
					
					std::string l = expressions.back();
					expressions.pop_back();
				
				    std::string opr, opl;	
				    if( l.size() > 1 ){
						opl  = "("+ l + ")";
					}
					else{
						opl += l;
					}	
					
					if ( r != "" ){
						if( r.size() > 1 )
							opr = "¬(" + r + ")";
						else
							opr =  "¬"+ r   ;
					}
				
					std::string result;
					result = "¬(" + opr + "^" + opl + ")";
					expressions.push_back(result);
				}
			}

			std::string createUntilExpression(bool isE = false){
			
				if ( !isE){
				   
				    std::string r;
				
					if (expressions.size() > 1 ){
						r = expressions.back();
						expressions.pop_back();
					}
					
					std::string l = expressions.back();
					expressions.pop_back();
				
				    std::string opr, opl;	
				    if( l.size() > 1 ){
						opl  = "("+ l + ")";
					}
					else{
						opl += l;
					}	
					
					if ( r != "" ){
						if( r.size() > 1 )
							opr = "(" + r + ")";
						else
							opr =   r   ;
					}
					return ("AF" + opr + "^¬E[¬"+ opr + "U(" + "¬" 
								+ opl + "^¬" + opr +")]");
				}
				else{
				
				    std::string r;
				
					if (expressions.size() > 1 ){
						r = expressions.back();
						expressions.pop_back();
					}
					
					std::string l = expressions.back();
					expressions.pop_back();
				
					std::string exp = "E[";
					if( l.size() > 1 ){
						exp += "("+ l + ")";
					}
					else{
						exp += l;
					}	
					
					if ( r != "" ){
						if( r.size() > 1 )
							exp += "U(" + r + ")]";
						else
							exp += "U" + r + "]" ;
					}
				
					return exp;
				}
			}
		
			/*
			void analysisElement(std::string elem, std::vector<std::string> &stack){
				if( elem != "" ){
					stack.push_back(elem);
				}
				else{
					std::string exp = expressions.back();
					stack.push_back(exp);
				}
			}
			*/
	};

	template <typename Iterator>
	struct replacer : qi::grammar<Iterator, std::string()> {
		replacer() : replacer::base_type(expression) {
			using qi::int_;
			using qi::_val;
			using qi::lit;
        	using qi::double_;
        	using qi::lexeme;
			using qi::eps;
			using qi::ascii::char_;
			using qi::ascii::string;

			property = 
				char_("a-ux-zB-DH-Z"); 

			term =
				eps >>
				( 
					(
						lit("¬") 
						>>
						term[boost::bind(&SemanticActionExpressionSubstitution::notExp,&sAction,_1)]
				    )	
					|
					factor
				)
				;

			factor =
				eps >>
				(
					property [boost::bind(&SemanticActionExpressionSubstitution::prop,&sAction,_1)]
					|
                	function
					|
					lit('(') >> expression >> lit(')')
				)
				;
	
			ag = 
				( string("AG") >> term [boost::bind(&SemanticActionExpressionSubstitution::ag,&sAction,_1)] );
			
			ax =
				( string("AX") >> term [boost::bind(&SemanticActionExpressionSubstitution::ax,&sAction,_1)] );

			af =
				( string("AF") >> term [boost::bind(&SemanticActionExpressionSubstitution::af,&sAction,_1)] );

			apuq = 
				( string("A[") 
							>> term 
							>> char_('U') 
						    >> term 
							>> char_(']') ) 
						[ 	
							boost::phoenix::ref(l)=qi::_3,
						  	boost::phoenix::ref(r)=qi::_5,
						  	boost::bind(&SemanticActionExpressionSubstitution::apUq,&sAction,l,r)
						];
		
			ef =
				( string("EF") >> term [boost::bind(&SemanticActionExpressionSubstitution::ef,&sAction,_1)] );				
		
			ex =
				( string("EX") >> term [boost::bind(&SemanticActionExpressionSubstitution::ex,&sAction,_1)] );				
			
			eg =
				( string("EG") >> term [ boost::bind(&SemanticActionExpressionSubstitution::eg,&sAction,_1) ] );				
			
			epuq = 
				( string("E[") 
							>> term 
							>> char_('U') 
							>> term 
							>> char_(']') ) 
						[ 	
							boost::phoenix::ref(l)=qi::_3,
						  	boost::phoenix::ref(r)=qi::_5,
						  	boost::bind(&SemanticActionExpressionSubstitution::epUq,&sAction,l,r)
						];
		
			function = 
				ef | ex | eg 
				|
				af | ax | ag
				|
				apuq 
				| 
				epuq
				;		
			
		   impliesExp = 
				term [boost::bind(&SemanticActionExpressionSubstitution::impliesExp,&sAction,_1,false)]
					>> *( char_('-') >> char_('>') 
				    >> term  [boost::bind(&SemanticActionExpressionSubstitution::impliesExp,&sAction,_1,true)]);

			andExp = 
				impliesExp [boost::bind(&SemanticActionExpressionSubstitution::andExp,&sAction,_1,false)]  
					>> *( char_('^') 
					>> impliesExp [boost::bind(&SemanticActionExpressionSubstitution::andExp,&sAction,_1,true)] );
			
			orExp = 
				andExp [boost::bind(&SemanticActionExpressionSubstitution::orExp,&sAction,_1,false)]  
					>> *( char_('v') 
					>> andExp [boost::bind(&SemanticActionExpressionSubstitution::orExp,&sAction,_1,true)] );
            
			expression =
				orExp;
				
		}

		std::string getResult(){
			return sAction.getExpression();
		}

		qi::rule<Iterator, std::string() > expression, factor, term, property;
		qi::rule<Iterator, std::string() > orExp , andExp, implies,impliesExp;
		qi::rule<Iterator, std::string() > function, apuq, epuq;
		qi::rule<Iterator, std::string() > ax, ex, af, ef, ag, eg;
		SemanticActionExpressionSubstitution sAction;
		std::string l, r;
	};
}

int main(int argc,char **argv){

	std::string expression, mac;

	try{
 		namespace po = boost::program_options;
		bool flagE = false, flagM = false;	
		po::options_description desc("Allowed options");
		desc.add_options()
			("help,h", "produces help message")
        	("expression,e", po::value<std::string>(), "<ctl expression>")
        	("machine,m", po::value<std::string>(), "<machine in graphviz format>")
		;	

		po::variables_map vm;
		po::store(po::parse_command_line(argc, argv, desc), vm);
		po::notify(vm);

		if (vm.count("help")) {
            std::cout << desc << std::endl;
            return 1;
        }
        
		if ( vm.count("expression") ) {
            expression =  vm["expression"].as<std::string>();
        } else {
			flagE = true;
        }

		if (vm.count("machine")) { 
        	mac  = vm["machine"].as<std::string>();
        } else {
			flagM = true;
        }

		if( flagE || flagM ){
            std::cout << desc << std::endl;
            return 1;
		}
	}
	catch(std::exception& e) {
        std::cerr << "error: " << e.what() << "\n";
        return 1;
    }
    catch(...) {
        std::cerr << "Exception of unknown type!\n";
    }

	typedef std::string::const_iterator iterator_type;
    typedef ctlReplacer::replacer<iterator_type> Replacer;
    typedef ctlAnalyser::analyser<iterator_type> Analyser;
	
	Replacer parser;

	std::string str(expression);

	std::string::const_iterator iter = str.begin();
    std::string::const_iterator end = str.end();	
	std::string result;
	
    std::cout << "----------------------------------------------------------\n";
	std::cout << "Transform the ctl expression " << str << " using the minimun set" << std::endl;
	std::cout << "The minimum set is {T, ¬, ^, EX, AF, EU}" << std::endl;	

	bool r = parse(iter, end, parser);
    
	if (r && iter == end) {
        std::cout << "----------------------------------------------------------\n";
        std::cout << "Expression with minimun set: " << std::endl;
        result = parser.getResult();
		std::cout << result << std::endl;
        std::cout << "----------------------------------------------------------\n";
    		
		Analyser analyser(mac);
		iter = result.begin();	
		end  = result.end();	
		bool x = parse(iter, end, analyser);
		if( x && iter == end){
			analyser.getAllMarks();
			analyser.getAllMarksByState();
			analyser.getResult(expression);
		}
		else{
			std::string rest(iter, end);
        	std::cerr << "----------------------------------------------------------\n";
        	std::cerr << "Transforming can't be done\n";
        	std::cerr << "stopped at: \": " << rest << "\"\n";
    		std::cerr << "----------------------------------------------------------\n";
		}
	}
    else {
        std::string rest(iter, end);
        std::cerr << "----------------------------------------------------------\n";
        std::cerr << "Transforming can't be done\n";
        std::cerr << "stopped at: \": " << rest << "\"\n";
    	std::cerr << "----------------------------------------------------------\n";
    }
	
	return 0;
}
